Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

\(x, x) → e
/(x, x) → e
.(e, x) → x
.(x, e) → x
\(e, x) → x
/(x, e) → x
.(x, \(x, y)) → y
.(/(y, x), x) → y
\(x, .(x, y)) → y
/(.(y, x), x) → y
/(x, \(y, x)) → y
\(/(x, y), x) → y

Q is empty.


QTRS
  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

\(x, x) → e
/(x, x) → e
.(e, x) → x
.(x, e) → x
\(e, x) → x
/(x, e) → x
.(x, \(x, y)) → y
.(/(y, x), x) → y
\(x, .(x, y)) → y
/(.(y, x), x) → y
/(x, \(y, x)) → y
\(/(x, y), x) → y

Q is empty.

We use [23] with the following order to prove termination.

Lexicographic path order with status [19].
Quasi-Precedence:
/2 > [\2, e]
.2 > [\2, e]

Status:
e: multiset
\2: [2,1]
.2: multiset
/2: [2,1]